package project2;

import java.util.LinkedList;
import java.util.Random;

public class ClauseForm
{

	boolean	traceMode;

	public ClauseForm(boolean traceMode)
	{
		super();
		this.traceMode = traceMode;

	}

	public void clauseForm(String input)
	{
		String step1 = calculateStep1(input); // eliminate <=>
		String step2 = calculateStep2(step1); // eliminate =>
		String step3 = calculateStep3(step2); // push ! inwards
		String step4 = calculateStep4(step3); // Standardise variables
		String step5 = calculateStep5(step4); // push quantifiers to left
		String step6 = calculateStep6(step5); // remove E
		String step7 = calculateStep7(step6); // remove quantifiers
	}

	public String calculateStep1(String input)
	{
		String step1 = eliminateEquivalence(input);
		while (step1.contains("<=>"))
		{
			step1 = eliminateEquivalence(step1);
		}
		if (traceMode)
			System.out.println("step1 " + step1);
		return step1;
	}

	public String eliminateEquivalence(String input)
	{
		String result = input;

		for (int i = 0; i < input.length(); i++)
		{

			if (input.charAt(i) == '<' && input.charAt(i + 1) == '=')
			{
				String[] eliminatedImplications = new String[2];
				eliminatedImplications[0] = input.substring(0, i);
				eliminatedImplications[1] = input.substring(i + 3,
						input.length());
				result = addingImplication(eliminatedImplications[0],
						eliminatedImplications[1]);

				return result;
			}
		}

		return result;
	}

	public String addingImplication(String beforeEqu, String afterEqu)
	{
		String result = "";
		String firstTerm = "";
		int count = 0;
		int i = beforeEqu.length() - 1;
		do
		{
			if (beforeEqu.charAt(i) == ')')
				count++;
			if (beforeEqu.charAt(i) == '(')
				count--;

			firstTerm = beforeEqu.charAt(i) + firstTerm;
			i--;
		} while (count != 0 && i > 0);

		if (i > 0
				&& ((int) beforeEqu.charAt(i) >= 65 && (int) beforeEqu
						.charAt(i) <= 90))
		{
			firstTerm = beforeEqu.charAt(i) + firstTerm;
		}

		String secondTerm = "";
		int j = 0;
		do
		{
			if (afterEqu.charAt(j) == ')')
				count++;
			if (afterEqu.charAt(j) == '(')
				count--;

			secondTerm = secondTerm + afterEqu.charAt(j);
			j++;

		} while ((count != 0 && j < afterEqu.length())
				|| ((int) afterEqu.charAt(j - 1) >= 65 && (int) afterEqu
						.charAt(j - 1) <= 90));

		result = beforeEqu.substring(0, i) + firstTerm + "=>" + secondTerm
				+ "&" + secondTerm + "=>" + firstTerm + afterEqu.substring(j);
		return result;
	}

	// eliminate =>
	public String calculateStep2(String input)
	{
		String step2 = eliminateImplications(input);
		while (step2.contains("=>"))
		{
			step2 = eliminateImplications(step2);
		}
		if (traceMode)
			System.out.println("step2 " + step2);
		return step2;
	}

	public String eliminateImplications(String input)
	{
		String result = input;

		for (int i = 0; i < input.length(); i++)
		{

			if (input.charAt(i) == '=' && input.charAt(i + 1) == '>')
			{
				String[] eliminatedImplications = new String[2];
				eliminatedImplications[0] = input.substring(0, i);
				eliminatedImplications[1] = input.substring(i + 2,
						input.length());
				eliminatedImplications[0] = addNot(eliminatedImplications[0]);
				result = eliminatedImplications[0] + "v"
						+ eliminatedImplications[1];
				return result;
			}
		}

		return result;
	}

	public String addNot(String input)
	{
		String result = "";
		int count = 0;
		int i = input.length() - 1;
		do
		{
			if (input.charAt(i) == ')')
				count++;
			if (input.charAt(i) == '(')
				count--;
			result = input.charAt(i) + result;
			i--;
		} while (count != 0 && i > 0);
		if (i > 0 && (input.charAt(i - 1) == 'A' || input.charAt(i - 1) == 'E'))
		{
			result = input.substring(0, i - 1) + "!" + input.charAt(i - 1)
					+ input.charAt(i) + result;
		}
		else
		{
			if (i > 0)

			{
				result = input.substring(0, i) + "!" + input.charAt(i) + result;
			}
			else
				result = "!" + input.charAt(i) + result;
		}
		return result;
	}

	public String calculateStep3(String step2)
	{
		String step3 = moveNegation(step2);
		while (step3.contains("!A") || step3.contains("!E"))
		{
			step3 = moveNegation(step3);
		}
		int count = 0;
		while (step3.contains("!(") && count < 5)
		{
			step3 = modifyNot(step3);
			count++;
		}

		step3 = step3.replace("!!", "");
		if (traceMode)
			System.out.println("step3 " + step3);

		return step3;
	}

	/**
	 * related to step3
	 * 
	 * @param input
	 * @return the string after moving the negation after the A and E and
	 *         replacing each A with an E and vice versa
	 */
	public String moveNegation(String input)
	{

		String result = "";
		input = input.replace("!!", "");

		for (int i = 0; i < input.length(); i++)
		{
			if (input.charAt(i) == '!'
					&& (input.charAt(i + 1) == 'E' || input.charAt(i + 1) == 'A'))
			{
				String[] temp = removeNot(input.substring(i));
				result = result + temp[0]
						+ input.substring(Integer.parseInt(temp[1]) + i);
				break;

			}
			else
			{

				result = result + input.charAt(i);
			}

		}
		return result;
	}

	/**
	 * related to step3
	 * 
	 * @param remainingString
	 * @return String [] result This method takes the string starting from the !
	 *         to the end of the sentence then it removes the ! before E& A and
	 *         puts it after the variable and it replaces E with A and A with E
	 *         result[0] contains the modified sentence result[1] is the index
	 *         of the "("
	 */
	public String[] removeNot(String remainingString)
	{
		String[] result = new String[2];
		result[0] = "";
		for (int i = 1; i < remainingString.length() - 1; i++)
		{
			if (remainingString.charAt(i + 1) == '(')
			{
				result[0] = result[0] + remainingString.charAt(i) + "!";
				result[1] = "" + (i + 1);
				break;
			}
			else
			{
				if (remainingString.charAt(i) == 'A')
				{
					result[0] = result[0] + "E";
				}
				else
					if (remainingString.charAt(i) == 'E')
					{
						result[0] = result[0] + "A";
					}
					else
						result[0] = result[0] + remainingString.charAt(i);

			}

		}
		return result;
	}

	public String modifyNot(String input)
	{
		String result = "";
		int count = 0;
		int i = input.length() - 1;
		do
		{

			if (input.charAt(i) == '('
					&& ((int) input.charAt(i - 1) < 97 || (int) input
							.charAt(i - 1) > 122))
			{
				// System.out.println("ana hena "+ input.charAt(i-1)
				// +input.charAt(i));
				count++;
				result = "!" + input.charAt(i - 1) + input.charAt(i) + result;
				// System.out.println(result);
				i--;
			}

			else
			{
				if (input.charAt(i) == ')')
				{
					count--;
					result = input.charAt(i) + result;
				}

				else
				{
					if (input.charAt(i) == 'v')
						result = "&" + result;
					else
					{
						if (input.charAt(i) == '&')
							result = "v" + result;
						else
							if (input.charAt(i) != '!')
								result = input.charAt(i) + result;
					}
				}
			}
			i--;
		} while (count != 0 && i > 0);

		result = input.substring(0, i + 1) + result;

		return result;
	}

	public String calculateStep4(String step2)
	{
		String quantifiers = "";
		char lastChar = step2.charAt(step2.length() - 1);

		for (int i = 0; i < step2.length() - 1; i++)
		{
			char c = step2.charAt(i);
			if (c == 'A' | c == 'E')
			{
				char c1 = step2.charAt(i + 1);
				// System.out.println("Quantifier " + c1);
				if (!quantifiers.contains("" + c1))
				{
					// System.out.println("First occurance for variable " + c1);
					quantifiers += c1;
				}
				else
				{
					char temp = this.generateRandomChar(step2);
					// System.out.println("Random character is : " + temp);
					String part1 = step2.substring(0, i);
					// System.out.println("part1 " + part1);
					String part2 = step2.substring(i, step2.length() - 1);
					// System.out.println("part2 " + part2);
					String newPart = part2.replace(c1, temp);
					// System.out.println("new part2 : " + newPart);
					step2 = part1.concat(newPart);
				}
			}
		}
		step2 = step2.concat("" + lastChar);
		if (traceMode)
			System.out.println("step4 " + step2);
		return step2;
	}

	public char generateRandomChar(String input)
	{
		Random r = new Random();
		char temp = (char) (r.nextInt(26) + 'a');
		if (input.contains("" + temp))
		{
			generateRandomChar(input);
		}
		else
		{
			return temp;
		}
		return temp;
	}

	/**
	 * related to step 5 :- moving quantifiers to the left loops over the input
	 * string and removes all quantifiers with all their variables and places
	 * them in a list then it concats the list with the input
	 */
	public String calculateStep5(String input)
	{
		LinkedList<String> quant = new LinkedList<String>();

		for (int i = 0; i < input.length(); i++)
		{
			if (input.charAt(i) == 'A' || input.charAt(i) == 'E')
			{
				quant.addLast("" + input.charAt(i) + input.charAt(i + 1));
				input = input.substring(0, i) + input.substring(i + 2);
				i = i - 1;
			}
		}
		for (int i = quant.size() - 1; i >= 0; i--)
		{
			input = quant.get(i) + input;
		}
		if (traceMode)
			System.out.println("step5 " + input);

		return input;
	}

	/**
	 * related to step 6 :- eliminate E replaces every variable of the E with
	 * sub(variable of the first A)
	 */
	// ask about law kza E 2l value 2lly hasibtitute biha htb2a
	public String calculateStep6(String input)
	{
		for (int i = 0; i < input.length(); i++)
		{
			if (input.charAt(i) == 'E')
			{
				String var = "" + input.charAt(i + 1);
				char var2 = input.charAt(input.indexOf("A") + 1);
				input = input.substring(0, i) + input.substring(i + 2);
				input = input.replace(var, "sub(" + var2 + ")");
				i = i - 1;
			}
		}

		if (traceMode)
			System.out.println("step6 " + input);
		return input;
	}

	/**
	 * related to step 7
	 * 
	 * @param args
	 */
	public String calculateStep7(String input)
	{
		int lastIndex = input.lastIndexOf("" + 'A');
		input = input.substring(lastIndex + 2);
		if (traceMode)
			System.out.println("step7 " + input);
		return input;
	}

	public static void main(String[] args)
	{

		/**
		 * => implication v or & and ! Not x,y,z variables P,Q,F functions E for
		 * every A for all () or [] brackets
		 */

		// take input from user
		String input = " (!(P(x)<=>Q(x))) &  (P(x,y))";
		// String input = "Ax(Ex(P(x)=>R(x))=>Ex(L(x)=>Q(x)))=>R(y)";
		// String input = "Ax(Q(x)) && Ey(R(y)) && Ez(P(z)) )";
		boolean trace = true;
		ClauseForm cF = new ClauseForm(trace);
		cF.clauseForm(input);
	}
}
